0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 32 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 67 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 19 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPOrderProof (⇔, 52 ms)
↳22 QDP
↳23 DependencyGraphProof (⇔, 0 ms)
↳24 TRUE
transposeD_in_ag(cons(T28, T29), cons(T26, T27)) → U7_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, X35, X36, T29) → U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_in_aggaa(T28, T26, T27, X35, X36))
row2colC_in_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
row2colA_in_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
row2colA_in_agaa(nil, nil, nil, nil) → row2colA_out_agaa(nil, nil, nil, nil)
U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_out_agaa(T86, T85, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140))
U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_out_agaa(T61, T60, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92))
U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_out_aggaa(T28, T26, T27, X35, X36)) → pB_out_aggaaa(T28, T26, T27, X35, X36, T29)
pB_in_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
pB_in_aggaaa(T28, T26, T27, T129, T129, nil) → U5_aggaaa(T28, T26, T27, T129, row2colC_in_aggaa(T28, T26, T27, T129, T129))
U5_aggaaa(T28, T26, T27, T129, row2colC_out_aggaa(T28, T26, T27, T129, T129)) → pB_out_aggaaa(T28, T26, T27, T129, T129, nil)
U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → pB_out_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122))
U7_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeD_out_ag(cons(T28, T29), cons(T26, T27))
transposeD_in_ag(nil, nil) → transposeD_out_ag(nil, nil)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
transposeD_in_ag(cons(T28, T29), cons(T26, T27)) → U7_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, X35, X36, T29) → U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_in_aggaa(T28, T26, T27, X35, X36))
row2colC_in_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
row2colA_in_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
row2colA_in_agaa(nil, nil, nil, nil) → row2colA_out_agaa(nil, nil, nil, nil)
U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_out_agaa(T86, T85, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140))
U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_out_agaa(T61, T60, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92))
U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_out_aggaa(T28, T26, T27, X35, X36)) → pB_out_aggaaa(T28, T26, T27, X35, X36, T29)
pB_in_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
pB_in_aggaaa(T28, T26, T27, T129, T129, nil) → U5_aggaaa(T28, T26, T27, T129, row2colC_in_aggaa(T28, T26, T27, T129, T129))
U5_aggaaa(T28, T26, T27, T129, row2colC_out_aggaa(T28, T26, T27, T129, T129)) → pB_out_aggaaa(T28, T26, T27, T129, T129, nil)
U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → pB_out_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122))
U7_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeD_out_ag(cons(T28, T29), cons(T26, T27))
transposeD_in_ag(nil, nil) → transposeD_out_ag(nil, nil)
TRANSPOSED_IN_AG(cons(T28, T29), cons(T26, T27)) → U7_AG(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
TRANSPOSED_IN_AG(cons(T28, T29), cons(T26, T27)) → PB_IN_AGGAAA(T28, T26, T27, X35, X36, T29)
PB_IN_AGGAAA(T28, T26, T27, X35, X36, T29) → U2_AGGAAA(T28, T26, T27, X35, X36, T29, row2colC_in_aggaa(T28, T26, T27, X35, X36))
PB_IN_AGGAAA(T28, T26, T27, X35, X36, T29) → ROW2COLC_IN_AGGAA(T28, T26, T27, X35, X36)
ROW2COLC_IN_AGGAA(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_AGGAA(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
ROW2COLC_IN_AGGAA(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → ROW2COLA_IN_AGAA(T61, T60, X91, X92)
ROW2COLA_IN_AGAA(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_AGAA(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
ROW2COLA_IN_AGAA(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → ROW2COLA_IN_AGAA(T86, T85, X139, X140)
PB_IN_AGGAAA(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
PB_IN_AGGAAA(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → ROW2COLC_IN_AGGAA(T28, T26, T27, cons(T119, T120), T118)
U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → U4_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → PB_IN_AGGAAA(T121, T119, T120, X185, X186, T122)
PB_IN_AGGAAA(T28, T26, T27, T129, T129, nil) → U5_AGGAAA(T28, T26, T27, T129, row2colC_in_aggaa(T28, T26, T27, T129, T129))
PB_IN_AGGAAA(T28, T26, T27, T129, T129, nil) → ROW2COLC_IN_AGGAA(T28, T26, T27, T129, T129)
transposeD_in_ag(cons(T28, T29), cons(T26, T27)) → U7_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, X35, X36, T29) → U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_in_aggaa(T28, T26, T27, X35, X36))
row2colC_in_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
row2colA_in_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
row2colA_in_agaa(nil, nil, nil, nil) → row2colA_out_agaa(nil, nil, nil, nil)
U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_out_agaa(T86, T85, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140))
U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_out_agaa(T61, T60, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92))
U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_out_aggaa(T28, T26, T27, X35, X36)) → pB_out_aggaaa(T28, T26, T27, X35, X36, T29)
pB_in_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
pB_in_aggaaa(T28, T26, T27, T129, T129, nil) → U5_aggaaa(T28, T26, T27, T129, row2colC_in_aggaa(T28, T26, T27, T129, T129))
U5_aggaaa(T28, T26, T27, T129, row2colC_out_aggaa(T28, T26, T27, T129, T129)) → pB_out_aggaaa(T28, T26, T27, T129, T129, nil)
U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → pB_out_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122))
U7_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeD_out_ag(cons(T28, T29), cons(T26, T27))
transposeD_in_ag(nil, nil) → transposeD_out_ag(nil, nil)
TRANSPOSED_IN_AG(cons(T28, T29), cons(T26, T27)) → U7_AG(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
TRANSPOSED_IN_AG(cons(T28, T29), cons(T26, T27)) → PB_IN_AGGAAA(T28, T26, T27, X35, X36, T29)
PB_IN_AGGAAA(T28, T26, T27, X35, X36, T29) → U2_AGGAAA(T28, T26, T27, X35, X36, T29, row2colC_in_aggaa(T28, T26, T27, X35, X36))
PB_IN_AGGAAA(T28, T26, T27, X35, X36, T29) → ROW2COLC_IN_AGGAA(T28, T26, T27, X35, X36)
ROW2COLC_IN_AGGAA(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_AGGAA(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
ROW2COLC_IN_AGGAA(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → ROW2COLA_IN_AGAA(T61, T60, X91, X92)
ROW2COLA_IN_AGAA(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_AGAA(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
ROW2COLA_IN_AGAA(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → ROW2COLA_IN_AGAA(T86, T85, X139, X140)
PB_IN_AGGAAA(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
PB_IN_AGGAAA(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → ROW2COLC_IN_AGGAA(T28, T26, T27, cons(T119, T120), T118)
U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → U4_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → PB_IN_AGGAAA(T121, T119, T120, X185, X186, T122)
PB_IN_AGGAAA(T28, T26, T27, T129, T129, nil) → U5_AGGAAA(T28, T26, T27, T129, row2colC_in_aggaa(T28, T26, T27, T129, T129))
PB_IN_AGGAAA(T28, T26, T27, T129, T129, nil) → ROW2COLC_IN_AGGAA(T28, T26, T27, T129, T129)
transposeD_in_ag(cons(T28, T29), cons(T26, T27)) → U7_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, X35, X36, T29) → U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_in_aggaa(T28, T26, T27, X35, X36))
row2colC_in_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
row2colA_in_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
row2colA_in_agaa(nil, nil, nil, nil) → row2colA_out_agaa(nil, nil, nil, nil)
U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_out_agaa(T86, T85, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140))
U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_out_agaa(T61, T60, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92))
U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_out_aggaa(T28, T26, T27, X35, X36)) → pB_out_aggaaa(T28, T26, T27, X35, X36, T29)
pB_in_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
pB_in_aggaaa(T28, T26, T27, T129, T129, nil) → U5_aggaaa(T28, T26, T27, T129, row2colC_in_aggaa(T28, T26, T27, T129, T129))
U5_aggaaa(T28, T26, T27, T129, row2colC_out_aggaa(T28, T26, T27, T129, T129)) → pB_out_aggaaa(T28, T26, T27, T129, T129, nil)
U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → pB_out_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122))
U7_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeD_out_ag(cons(T28, T29), cons(T26, T27))
transposeD_in_ag(nil, nil) → transposeD_out_ag(nil, nil)
ROW2COLA_IN_AGAA(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → ROW2COLA_IN_AGAA(T86, T85, X139, X140)
transposeD_in_ag(cons(T28, T29), cons(T26, T27)) → U7_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, X35, X36, T29) → U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_in_aggaa(T28, T26, T27, X35, X36))
row2colC_in_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
row2colA_in_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
row2colA_in_agaa(nil, nil, nil, nil) → row2colA_out_agaa(nil, nil, nil, nil)
U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_out_agaa(T86, T85, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140))
U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_out_agaa(T61, T60, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92))
U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_out_aggaa(T28, T26, T27, X35, X36)) → pB_out_aggaaa(T28, T26, T27, X35, X36, T29)
pB_in_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
pB_in_aggaaa(T28, T26, T27, T129, T129, nil) → U5_aggaaa(T28, T26, T27, T129, row2colC_in_aggaa(T28, T26, T27, T129, T129))
U5_aggaaa(T28, T26, T27, T129, row2colC_out_aggaa(T28, T26, T27, T129, T129)) → pB_out_aggaaa(T28, T26, T27, T129, T129, nil)
U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → pB_out_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122))
U7_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeD_out_ag(cons(T28, T29), cons(T26, T27))
transposeD_in_ag(nil, nil) → transposeD_out_ag(nil, nil)
ROW2COLA_IN_AGAA(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → ROW2COLA_IN_AGAA(T86, T85, X139, X140)
ROW2COLA_IN_AGAA(cons(cons(T82, T84), T85)) → ROW2COLA_IN_AGAA(T85)
From the DPs we obtained the following set of size-change graphs:
PB_IN_AGGAAA(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → PB_IN_AGGAAA(T121, T119, T120, X185, X186, T122)
transposeD_in_ag(cons(T28, T29), cons(T26, T27)) → U7_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, X35, X36, T29) → U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_in_aggaa(T28, T26, T27, X35, X36))
row2colC_in_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
row2colA_in_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
row2colA_in_agaa(nil, nil, nil, nil) → row2colA_out_agaa(nil, nil, nil, nil)
U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_out_agaa(T86, T85, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140))
U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_out_agaa(T61, T60, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92))
U2_aggaaa(T28, T26, T27, X35, X36, T29, row2colC_out_aggaa(T28, T26, T27, X35, X36)) → pB_out_aggaaa(T28, T26, T27, X35, X36, T29)
pB_in_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
U3_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
pB_in_aggaaa(T28, T26, T27, T129, T129, nil) → U5_aggaaa(T28, T26, T27, T129, row2colC_in_aggaa(T28, T26, T27, T129, T129))
U5_aggaaa(T28, T26, T27, T129, row2colC_out_aggaa(T28, T26, T27, T129, T129)) → pB_out_aggaaa(T28, T26, T27, T129, T129, nil)
U4_aggaaa(T28, T26, T27, T119, T120, T118, T121, T122, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → pB_out_aggaaa(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122))
U7_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeD_out_ag(cons(T28, T29), cons(T26, T27))
transposeD_in_ag(nil, nil) → transposeD_out_ag(nil, nil)
PB_IN_AGGAAA(T28, T26, T27, cons(T119, T120), T118, cons(T121, T122)) → U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_in_aggaa(T28, T26, T27, cons(T119, T120), T118))
U3_AGGAAA(T28, T26, T27, T119, T120, T118, T121, T122, row2colC_out_aggaa(T28, T26, T27, cons(T119, T120), T118)) → PB_IN_AGGAAA(T121, T119, T120, X185, X186, T122)
row2colC_in_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92)) → U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_in_agaa(T61, T60, X91, X92))
U6_aggaa(T57, T61, T59, T60, X91, X92, row2colA_out_agaa(T61, T60, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T57, T59), T60, cons(T59, X91), cons(nil, X92))
row2colA_in_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140)) → U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_in_agaa(T86, T85, X139, X140))
row2colA_in_agaa(nil, nil, nil, nil) → row2colA_out_agaa(nil, nil, nil, nil)
U1_agaa(T82, T86, T84, T85, X139, X140, row2colA_out_agaa(T86, T85, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(cons(T82, T84), T85), cons(T84, X139), cons(nil, X140))
PB_IN_AGGAAA(T26, T27) → U3_AGGAAA(row2colC_in_aggaa(T26, T27))
U3_AGGAAA(row2colC_out_aggaa(T28, cons(T119, T120), T118)) → PB_IN_AGGAAA(T119, T120)
row2colC_in_aggaa(cons(T57, T59), T60) → U6_aggaa(T57, T59, row2colA_in_agaa(T60))
U6_aggaa(T57, T59, row2colA_out_agaa(T61, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T59, X91), cons(nil, X92))
row2colA_in_agaa(cons(cons(T82, T84), T85)) → U1_agaa(T82, T84, row2colA_in_agaa(T85))
row2colA_in_agaa(nil) → row2colA_out_agaa(nil, nil, nil)
U1_agaa(T82, T84, row2colA_out_agaa(T86, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(T84, X139), cons(nil, X140))
row2colC_in_aggaa(x0, x1)
U6_aggaa(x0, x1, x2)
row2colA_in_agaa(x0)
U1_agaa(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U3_AGGAAA(row2colC_out_aggaa(T28, cons(T119, T120), T118)) → PB_IN_AGGAAA(T119, T120)
POL(PB_IN_AGGAAA(x1, x2)) = x1 + x2
POL(U1_agaa(x1, x2, x3)) = 1 + x2 + x3
POL(U3_AGGAAA(x1)) = x1
POL(U6_aggaa(x1, x2, x3)) = 1 + x2 + x3
POL(cons(x1, x2)) = 1 + x1 + x2
POL(nil) = 0
POL(row2colA_in_agaa(x1)) = x1
POL(row2colA_out_agaa(x1, x2, x3)) = x2
POL(row2colC_in_aggaa(x1, x2)) = x1 + x2
POL(row2colC_out_aggaa(x1, x2, x3)) = x2
row2colC_in_aggaa(cons(T57, T59), T60) → U6_aggaa(T57, T59, row2colA_in_agaa(T60))
row2colA_in_agaa(cons(cons(T82, T84), T85)) → U1_agaa(T82, T84, row2colA_in_agaa(T85))
row2colA_in_agaa(nil) → row2colA_out_agaa(nil, nil, nil)
U6_aggaa(T57, T59, row2colA_out_agaa(T61, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T59, X91), cons(nil, X92))
U1_agaa(T82, T84, row2colA_out_agaa(T86, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(T84, X139), cons(nil, X140))
PB_IN_AGGAAA(T26, T27) → U3_AGGAAA(row2colC_in_aggaa(T26, T27))
row2colC_in_aggaa(cons(T57, T59), T60) → U6_aggaa(T57, T59, row2colA_in_agaa(T60))
U6_aggaa(T57, T59, row2colA_out_agaa(T61, X91, X92)) → row2colC_out_aggaa(cons(T57, T61), cons(T59, X91), cons(nil, X92))
row2colA_in_agaa(cons(cons(T82, T84), T85)) → U1_agaa(T82, T84, row2colA_in_agaa(T85))
row2colA_in_agaa(nil) → row2colA_out_agaa(nil, nil, nil)
U1_agaa(T82, T84, row2colA_out_agaa(T86, X139, X140)) → row2colA_out_agaa(cons(T82, T86), cons(T84, X139), cons(nil, X140))
row2colC_in_aggaa(x0, x1)
U6_aggaa(x0, x1, x2)
row2colA_in_agaa(x0)
U1_agaa(x0, x1, x2)